Termination proof of /tmp/tmpHk-HXX/countUpNo.itrs

Termination of the given ITRSProblem could not be shown:

↳ ITRS

  ↳ ITRStoIDPProof

ITRS problem:
The following domains are used:

z

The TRS R consists of the following rules:

cu(TRUE, x) → cu(<@z(x, exp(x)), +@z(x, 1@z))
exp(x) → *@z(2@z, x)

The set Q consists of the following terms:

cu(TRUE, x0)
exp(x0)

Added dependency pairs

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

cu(TRUE, x) → cu(<@z(x, exp(x)), +@z(x, 1@z))
exp(x) → *@z(2@z, x)

The integer pair graph contains the following rules and edges:

(0): CU(TRUE, x[0]) → CU(<@z(x[0], exp(x[0])), +@z(x[0], 1@z))
(1): CU(TRUE, x[1]) → EXP(x[1])

(0) -> (0), if ((+@z(x[0], 1@z) →^* x[0]a)∧(<@z(x[0], exp(x[0])) →^* TRUE))

(0) -> (1), if ((+@z(x[0], 1@z) →^* x[1])∧(<@z(x[0], exp(x[0])) →^* TRUE))

The set Q consists of the following terms:

cu(TRUE, x0)
exp(x0)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

exp(x) → *@z(2@z, x)

The integer pair graph contains the following rules and edges:

(0): CU(TRUE, x[0]) → CU(<@z(x[0], exp(x[0])), +@z(x[0], 1@z))
(1): CU(TRUE, x[1]) → EXP(x[1])

(0) -> (0), if ((+@z(x[0], 1@z) →^* x[0]a)∧(<@z(x[0], exp(x[0])) →^* TRUE))

(0) -> (1), if ((+@z(x[0], 1@z) →^* x[1])∧(<@z(x[0], exp(x[0])) →^* TRUE))

The set Q consists of the following terms:

cu(TRUE, x0)
exp(x0)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

exp(x) → *@z(2@z, x)

The integer pair graph contains the following rules and edges:

(0): CU(TRUE, x[0]) → CU(<@z(x[0], exp(x[0])), +@z(x[0], 1@z))

(0) -> (0), if ((+@z(x[0], 1@z) →^* x[0]a)∧(<@z(x[0], exp(x[0])) →^* TRUE))

The set Q consists of the following terms:

cu(TRUE, x0)
exp(x0)

Represented integers and predefined function symbols by Terms

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

CU(true, x[0]) → CU(less_int(x[0], exp(x[0])), plus_int(pos(s(0)), x[0]))

The TRS R consists of the following rules:

exp(x) → mult_int(pos(s(s(0))), x)
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), neg(0)) → false
less_int(neg(0), pos(0)) → false
less_int(neg(0), neg(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(neg(0), pos(s(y))) → true
less_int(pos(0), neg(s(y))) → false
less_int(neg(0), neg(s(y))) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
less_int(pos(s(x)), neg(0)) → false
less_int(neg(s(x)), neg(0)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

cu(true, x0)
exp(x0)
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

CU(true, x[0]) → CU(less_int(x[0], exp(x[0])), plus_int(pos(s(0)), x[0]))

The TRS R consists of the following rules:

exp(x) → mult_int(pos(s(s(0))), x)
less_int(pos(0), pos(0)) → false
less_int(pos(0), neg(0)) → false
less_int(neg(0), pos(0)) → false
less_int(neg(0), neg(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(neg(0), pos(s(y))) → true
less_int(pos(0), neg(s(y))) → false
less_int(neg(0), neg(s(y))) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
less_int(pos(s(x)), neg(0)) → false
less_int(neg(s(x)), neg(0)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))

The set Q consists of the following terms:

cu(true, x0)
exp(x0)
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

cu(true, x0)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

CU(true, x[0]) → CU(less_int(x[0], exp(x[0])), plus_int(pos(s(0)), x[0]))

The TRS R consists of the following rules:

exp(x) → mult_int(pos(s(s(0))), x)
less_int(pos(0), pos(0)) → false
less_int(pos(0), neg(0)) → false
less_int(neg(0), pos(0)) → false
less_int(neg(0), neg(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(neg(0), pos(s(y))) → true
less_int(pos(0), neg(s(y))) → false
less_int(neg(0), neg(s(y))) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
less_int(pos(s(x)), neg(0)) → false
less_int(neg(s(x)), neg(0)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))

The set Q consists of the following terms:

exp(x0)
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, x[0]) → CU(less_int(x[0], exp(x[0])), plus_int(pos(s(0)), x[0])) at position [0,1] we obtained the following new rules [LPAR04]:

CU(true, x[0]) → CU(less_int(x[0], mult_int(pos(s(s(0))), x[0])), plus_int(pos(s(0)), x[0]))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

CU(true, x[0]) → CU(less_int(x[0], mult_int(pos(s(s(0))), x[0])), plus_int(pos(s(0)), x[0]))

The TRS R consists of the following rules:

exp(x) → mult_int(pos(s(s(0))), x)
less_int(pos(0), pos(0)) → false
less_int(pos(0), neg(0)) → false
less_int(neg(0), pos(0)) → false
less_int(neg(0), neg(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(neg(0), pos(s(y))) → true
less_int(pos(0), neg(s(y))) → false
less_int(neg(0), neg(s(y))) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
less_int(pos(s(x)), neg(0)) → false
less_int(neg(s(x)), neg(0)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))

The set Q consists of the following terms:

exp(x0)
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

CU(true, x[0]) → CU(less_int(x[0], mult_int(pos(s(s(0))), x[0])), plus_int(pos(s(0)), x[0]))

The TRS R consists of the following rules:

mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), neg(0)) → false
less_int(neg(0), pos(0)) → false
less_int(neg(0), neg(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(neg(0), pos(s(y))) → true
less_int(pos(0), neg(s(y))) → false
less_int(neg(0), neg(s(y))) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
less_int(pos(s(x)), neg(0)) → false
less_int(neg(s(x)), neg(0)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))

The set Q consists of the following terms:

exp(x0)
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

exp(x0)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

CU(true, x[0]) → CU(less_int(x[0], mult_int(pos(s(s(0))), x[0])), plus_int(pos(s(0)), x[0]))

The TRS R consists of the following rules:

mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), neg(0)) → false
less_int(neg(0), pos(0)) → false
less_int(neg(0), neg(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(neg(0), pos(s(y))) → true
less_int(pos(0), neg(s(y))) → false
less_int(neg(0), neg(s(y))) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
less_int(pos(s(x)), neg(0)) → false
less_int(neg(s(x)), neg(0)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))

The set Q consists of the following terms:

mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
In the following pairs the term without variables pos(s(s(0))) is replaced by the fresh variable x_removed.
Pair: CU(true, x[0]) → CU(less_int(x[0], mult_int(pos(s(s(0))), x[0])), plus_int(pos(s(0)), x[0]))
Positions in right side of the pair:

[0,1,0]

The new variable was added to all pairs as a new argument[CONREM].

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                        ↳ QDP

                                      ↳ RemovalProof

                                      ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

CU(true, x[0], x_removed) → CU(less_int(x[0], mult_int(x_removed, x[0])), plus_int(pos(s(0)), x[0]), x_removed)

The TRS R consists of the following rules:

mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), neg(0)) → false
less_int(neg(0), pos(0)) → false
less_int(neg(0), neg(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(neg(0), pos(s(y))) → true
less_int(pos(0), neg(s(y))) → false
less_int(neg(0), neg(s(y))) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
less_int(pos(s(x)), neg(0)) → false
less_int(neg(s(x)), neg(0)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))

The set Q consists of the following terms:

mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

[0,1,0]

The new variable was added to all pairs as a new argument[CONREM].

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                        ↳ QDP

                                      ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

CU(true, x[0], x_removed) → CU(less_int(x[0], mult_int(x_removed, x[0])), plus_int(pos(s(0)), x[0]), x_removed)

The TRS R consists of the following rules:

mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), neg(0)) → false
less_int(neg(0), pos(0)) → false
less_int(neg(0), neg(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(neg(0), pos(s(y))) → true
less_int(pos(0), neg(s(y))) → false
less_int(neg(0), neg(s(y))) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
less_int(pos(s(x)), neg(0)) → false
less_int(neg(s(x)), neg(0)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))

The set Q consists of the following terms:

mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [LPAR04] the rule CU(true, x[0]) → CU(less_int(x[0], mult_int(pos(s(s(0))), x[0])), plus_int(pos(s(0)), x[0])) at position [0] we obtained the following new rules [LPAR04]:

CU(true, neg(x1)) → CU(less_int(neg(x1), neg(mult_nat(s(s(0)), x1))), plus_int(pos(s(0)), neg(x1)))
CU(true, pos(x1)) → CU(less_int(pos(x1), pos(mult_nat(s(s(0)), x1))), plus_int(pos(s(0)), pos(x1)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(x1)) → CU(less_int(neg(x1), neg(mult_nat(s(s(0)), x1))), plus_int(pos(s(0)), neg(x1)))
CU(true, pos(x1)) → CU(less_int(pos(x1), pos(mult_nat(s(s(0)), x1))), plus_int(pos(s(0)), pos(x1)))

The TRS R consists of the following rules:

mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), neg(0)) → false
less_int(neg(0), pos(0)) → false
less_int(neg(0), neg(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(neg(0), pos(s(y))) → true
less_int(pos(0), neg(s(y))) → false
less_int(neg(0), neg(s(y))) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
less_int(pos(s(x)), neg(0)) → false
less_int(neg(s(x)), neg(0)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))

The set Q consists of the following terms:

mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(x1)) → CU(less_int(neg(x1), neg(mult_nat(s(s(0)), x1))), plus_int(pos(s(0)), neg(x1)))
CU(true, pos(x1)) → CU(less_int(pos(x1), pos(mult_nat(s(s(0)), x1))), plus_int(pos(s(0)), pos(x1)))

The TRS R consists of the following rules:

mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))

The set Q consists of the following terms:

mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(x1)) → CU(less_int(neg(x1), neg(mult_nat(s(s(0)), x1))), plus_int(pos(s(0)), neg(x1)))
CU(true, pos(x1)) → CU(less_int(pos(x1), pos(mult_nat(s(s(0)), x1))), plus_int(pos(s(0)), pos(x1)))

The TRS R consists of the following rules:

mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, neg(x1)) → CU(less_int(neg(x1), neg(mult_nat(s(s(0)), x1))), plus_int(pos(s(0)), neg(x1))) at position [1] we obtained the following new rules [LPAR04]:

CU(true, neg(x1)) → CU(less_int(neg(x1), neg(mult_nat(s(s(0)), x1))), minus_nat(s(0), x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(x1)) → CU(less_int(pos(x1), pos(mult_nat(s(s(0)), x1))), plus_int(pos(s(0)), pos(x1)))
CU(true, neg(x1)) → CU(less_int(neg(x1), neg(mult_nat(s(s(0)), x1))), minus_nat(s(0), x1))

The TRS R consists of the following rules:

mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(x1)) → CU(less_int(pos(x1), pos(mult_nat(s(s(0)), x1))), plus_int(pos(s(0)), pos(x1)))
CU(true, neg(x1)) → CU(less_int(neg(x1), neg(mult_nat(s(s(0)), x1))), minus_nat(s(0), x1))

The TRS R consists of the following rules:

mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, pos(x1)) → CU(less_int(pos(x1), pos(mult_nat(s(s(0)), x1))), plus_int(pos(s(0)), pos(x1))) at position [1] we obtained the following new rules [LPAR04]:

CU(true, pos(x1)) → CU(less_int(pos(x1), pos(mult_nat(s(s(0)), x1))), pos(plus_nat(s(0), x1)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(x1)) → CU(less_int(neg(x1), neg(mult_nat(s(s(0)), x1))), minus_nat(s(0), x1))
CU(true, pos(x1)) → CU(less_int(pos(x1), pos(mult_nat(s(s(0)), x1))), pos(plus_nat(s(0), x1)))

The TRS R consists of the following rules:

mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(x1)) → CU(less_int(pos(x1), pos(mult_nat(s(s(0)), x1))), pos(plus_nat(s(0), x1)))

The TRS R consists of the following rules:

mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(x1)) → CU(less_int(pos(x1), pos(mult_nat(s(s(0)), x1))), pos(plus_nat(s(0), x1)))

The TRS R consists of the following rules:

mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_nat(0, x) → x
mult_nat(0, y) → 0

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Rewriting

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(x1)) → CU(less_int(pos(x1), pos(mult_nat(s(s(0)), x1))), pos(plus_nat(s(0), x1)))

The TRS R consists of the following rules:

mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_nat(0, x) → x
mult_nat(0, y) → 0

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, pos(x1)) → CU(less_int(pos(x1), pos(mult_nat(s(s(0)), x1))), pos(plus_nat(s(0), x1))) at position [1,0] we obtained the following new rules [LPAR04]:

CU(true, pos(x1)) → CU(less_int(pos(x1), pos(mult_nat(s(s(0)), x1))), pos(s(plus_nat(0, x1))))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Rewriting

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(x1)) → CU(less_int(pos(x1), pos(mult_nat(s(s(0)), x1))), pos(s(plus_nat(0, x1))))

The TRS R consists of the following rules:

mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_nat(0, x) → x
mult_nat(0, y) → 0

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, pos(x1)) → CU(less_int(pos(x1), pos(mult_nat(s(s(0)), x1))), pos(s(plus_nat(0, x1)))) at position [1,0,0] we obtained the following new rules [LPAR04]:

CU(true, pos(x1)) → CU(less_int(pos(x1), pos(mult_nat(s(s(0)), x1))), pos(s(x1)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Rewriting

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Instantiation

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(x1)) → CU(less_int(pos(x1), pos(mult_nat(s(s(0)), x1))), pos(s(x1)))

The TRS R consists of the following rules:

mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_nat(0, x) → x
mult_nat(0, y) → 0

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By instantiating [LPAR04] the rule CU(true, pos(x1)) → CU(less_int(pos(x1), pos(mult_nat(s(s(0)), x1))), pos(s(x1))) we obtained the following new rules [LPAR04]:

CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(mult_nat(s(s(0)), s(z0)))), pos(s(s(z0))))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Rewriting

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Instantiation

                                                                                      ↳ QDP

                                                                                        ↳ UsableRulesProof

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(mult_nat(s(s(0)), s(z0)))), pos(s(s(z0))))

The TRS R consists of the following rules:

mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_nat(0, x) → x
mult_nat(0, y) → 0

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Rewriting

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Instantiation

                                                                                      ↳ QDP

                                                                                        ↳ UsableRulesProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(mult_nat(s(s(0)), s(z0)))), pos(s(s(z0))))

The TRS R consists of the following rules:

mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true
mult_nat(0, y) → 0
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_nat(0, x) → x

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(mult_nat(s(s(0)), s(z0)))), pos(s(s(z0)))) at position [0,1,0] we obtained the following new rules [LPAR04]:

CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(plus_nat(mult_nat(s(0), s(z0)), s(z0)))), pos(s(s(z0))))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Rewriting

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Instantiation

                                                                                      ↳ QDP

                                                                                        ↳ UsableRulesProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(plus_nat(mult_nat(s(0), s(z0)), s(z0)))), pos(s(s(z0))))

The TRS R consists of the following rules:

mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true
mult_nat(0, y) → 0
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_nat(0, x) → x

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(plus_nat(mult_nat(s(0), s(z0)), s(z0)))), pos(s(s(z0)))) at position [0,1,0,0] we obtained the following new rules [LPAR04]:

CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(plus_nat(plus_nat(mult_nat(0, s(z0)), s(z0)), s(z0)))), pos(s(s(z0))))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Rewriting

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Instantiation

                                                                                      ↳ QDP

                                                                                        ↳ UsableRulesProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ UsableRulesProof

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(plus_nat(plus_nat(mult_nat(0, s(z0)), s(z0)), s(z0)))), pos(s(s(z0))))

The TRS R consists of the following rules:

mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true
mult_nat(0, y) → 0
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_nat(0, x) → x

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Rewriting

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Instantiation

                                                                                      ↳ QDP

                                                                                        ↳ UsableRulesProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ UsableRulesProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(plus_nat(plus_nat(mult_nat(0, s(z0)), s(z0)), s(z0)))), pos(s(s(z0))))

The TRS R consists of the following rules:

mult_nat(0, y) → 0
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_nat(0, x) → x
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(plus_nat(plus_nat(mult_nat(0, s(z0)), s(z0)), s(z0)))), pos(s(s(z0)))) at position [0,1,0,0,0] we obtained the following new rules [LPAR04]:

CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(plus_nat(plus_nat(0, s(z0)), s(z0)))), pos(s(s(z0))))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Rewriting

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Instantiation

                                                                                      ↳ QDP

                                                                                        ↳ UsableRulesProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ UsableRulesProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ UsableRulesProof

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(plus_nat(plus_nat(0, s(z0)), s(z0)))), pos(s(s(z0))))

The TRS R consists of the following rules:

mult_nat(0, y) → 0
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_nat(0, x) → x
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Rewriting

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Instantiation

                                                                                      ↳ QDP

                                                                                        ↳ UsableRulesProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ UsableRulesProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ UsableRulesProof

                                                                                                              ↳ QDP

                                                                                                                ↳ QReductionProof

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(plus_nat(plus_nat(0, s(z0)), s(z0)))), pos(s(s(z0))))

The TRS R consists of the following rules:

plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Rewriting

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Instantiation

                                                                                      ↳ QDP

                                                                                        ↳ UsableRulesProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ UsableRulesProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ UsableRulesProof

                                                                                                              ↳ QDP

                                                                                                                ↳ QReductionProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Rewriting

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(plus_nat(plus_nat(0, s(z0)), s(z0)))), pos(s(s(z0))))

The TRS R consists of the following rules:

plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true

The set Q consists of the following terms:

plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(plus_nat(plus_nat(0, s(z0)), s(z0)))), pos(s(s(z0)))) at position [0,1,0,0] we obtained the following new rules [LPAR04]:

CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(plus_nat(s(z0), s(z0)))), pos(s(s(z0))))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Rewriting

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Instantiation

                                                                                      ↳ QDP

                                                                                        ↳ UsableRulesProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ UsableRulesProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ UsableRulesProof

                                                                                                              ↳ QDP

                                                                                                                ↳ QReductionProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Rewriting

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Rewriting

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(plus_nat(s(z0), s(z0)))), pos(s(s(z0))))

The TRS R consists of the following rules:

plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true

The set Q consists of the following terms:

plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(plus_nat(s(z0), s(z0)))), pos(s(s(z0)))) at position [0,1,0] we obtained the following new rules [LPAR04]:

CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(s(plus_nat(z0, s(z0))))), pos(s(s(z0))))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Rewriting

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Instantiation

                                                                                      ↳ QDP

                                                                                        ↳ UsableRulesProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ UsableRulesProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ UsableRulesProof

                                                                                                              ↳ QDP

                                                                                                                ↳ QReductionProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Rewriting

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Rewriting

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(s(plus_nat(z0, s(z0))))), pos(s(s(z0))))

The TRS R consists of the following rules:

plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true

The set Q consists of the following terms:

plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, pos(s(z0))) → CU(less_int(pos(s(z0)), pos(s(plus_nat(z0, s(z0))))), pos(s(s(z0)))) at position [0] we obtained the following new rules [LPAR04]:

CU(true, pos(s(z0))) → CU(less_int(pos(z0), pos(plus_nat(z0, s(z0)))), pos(s(s(z0))))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Rewriting

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Instantiation

                                                                                      ↳ QDP

                                                                                        ↳ UsableRulesProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ UsableRulesProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ UsableRulesProof

                                                                                                              ↳ QDP

                                                                                                                ↳ QReductionProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Rewriting

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Rewriting

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(s(z0))) → CU(less_int(pos(z0), pos(plus_nat(z0, s(z0)))), pos(s(s(z0))))

The TRS R consists of the following rules:

plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true

The set Q consists of the following terms:

plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By instantiating [LPAR04] the rule CU(true, pos(s(z0))) → CU(less_int(pos(z0), pos(plus_nat(z0, s(z0)))), pos(s(s(z0)))) we obtained the following new rules [LPAR04]:

CU(true, pos(s(s(z0)))) → CU(less_int(pos(s(z0)), pos(plus_nat(s(z0), s(s(z0))))), pos(s(s(s(z0)))))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Rewriting

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Instantiation

                                                                                      ↳ QDP

                                                                                        ↳ UsableRulesProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ UsableRulesProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ UsableRulesProof

                                                                                                              ↳ QDP

                                                                                                                ↳ QReductionProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Rewriting

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Rewriting

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(s(s(z0)))) → CU(less_int(pos(s(z0)), pos(plus_nat(s(z0), s(s(z0))))), pos(s(s(s(z0)))))

The TRS R consists of the following rules:

plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true

The set Q consists of the following terms:

plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, pos(s(s(z0)))) → CU(less_int(pos(s(z0)), pos(plus_nat(s(z0), s(s(z0))))), pos(s(s(s(z0))))) at position [0,1,0] we obtained the following new rules [LPAR04]:

CU(true, pos(s(s(z0)))) → CU(less_int(pos(s(z0)), pos(s(plus_nat(z0, s(s(z0)))))), pos(s(s(s(z0)))))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Rewriting

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Instantiation

                                                                                      ↳ QDP

                                                                                        ↳ UsableRulesProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ UsableRulesProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ UsableRulesProof

                                                                                                              ↳ QDP

                                                                                                                ↳ QReductionProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Rewriting

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Rewriting

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(s(s(z0)))) → CU(less_int(pos(s(z0)), pos(s(plus_nat(z0, s(s(z0)))))), pos(s(s(s(z0)))))

The TRS R consists of the following rules:

plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true

The set Q consists of the following terms:

plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, pos(s(s(z0)))) → CU(less_int(pos(s(z0)), pos(s(plus_nat(z0, s(s(z0)))))), pos(s(s(s(z0))))) at position [0] we obtained the following new rules [LPAR04]:

CU(true, pos(s(s(z0)))) → CU(less_int(pos(z0), pos(plus_nat(z0, s(s(z0))))), pos(s(s(s(z0)))))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Rewriting

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Instantiation

                                                                                      ↳ QDP

                                                                                        ↳ UsableRulesProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ UsableRulesProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ UsableRulesProof

                                                                                                              ↳ QDP

                                                                                                                ↳ QReductionProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Rewriting

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Rewriting

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ QReductionProof

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(s(s(z0)))) → CU(less_int(pos(z0), pos(plus_nat(z0, s(s(z0))))), pos(s(s(s(z0)))))

The TRS R consists of the following rules:

plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true

The set Q consists of the following terms:

plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as they contain symbols which do neither occur in P nor in R.[THIEMANN].

less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Rewriting

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Instantiation

                                                                                      ↳ QDP

                                                                                        ↳ UsableRulesProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ UsableRulesProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ UsableRulesProof

                                                                                                              ↳ QDP

                                                                                                                ↳ QReductionProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Rewriting

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Rewriting

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ QReductionProof

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ MNOCProof

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(s(s(z0)))) → CU(less_int(pos(z0), pos(plus_nat(z0, s(s(z0))))), pos(s(s(s(z0)))))

The TRS R consists of the following rules:

plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true

The set Q consists of the following terms:

plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), pos(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(pos(s(x0)), pos(s(x1)))

We have to consider all (P,Q,R)-chains.
We use the modular non-overlap check [FROCOS05] to decrease Q to the empty set.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Rewriting

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Instantiation

                                                                                      ↳ QDP

                                                                                        ↳ UsableRulesProof

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ UsableRulesProof

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ UsableRulesProof

                                                                                                              ↳ QDP

                                                                                                                ↳ QReductionProof

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Rewriting

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Rewriting

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ QReductionProof

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ MNOCProof

                                                                                                                                                  ↳ QDP

                                                                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CU(true, pos(s(s(z0)))) → CU(less_int(pos(z0), pos(plus_nat(z0, s(s(z0))))), pos(s(s(s(z0)))))

The TRS R consists of the following rules:

plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true

Q is empty.
We have to consider all (P,Q,R)-chains.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(x1)) → CU(less_int(neg(x1), neg(mult_nat(s(s(0)), x1))), minus_nat(s(0), x1))

The TRS R consists of the following rules:

mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(pos(s(x)), pos(0)) → false
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(x1)) → CU(less_int(neg(x1), neg(mult_nat(s(s(0)), x1))), minus_nat(s(0), x1))

The TRS R consists of the following rules:

mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(x1)) → CU(less_int(neg(x1), neg(mult_nat(s(s(0)), x1))), minus_nat(s(0), x1))

The TRS R consists of the following rules:

mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [LPAR04] the rule CU(true, neg(x1)) → CU(less_int(neg(x1), neg(mult_nat(s(s(0)), x1))), minus_nat(s(0), x1)) at position [1] we obtained the following new rules [LPAR04]:

CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(mult_nat(s(s(0)), s(x1)))), minus_nat(0, x1))
CU(true, neg(0)) → CU(less_int(neg(0), neg(mult_nat(s(s(0)), 0))), pos(s(0)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(mult_nat(s(s(0)), s(x1)))), minus_nat(0, x1))
CU(true, neg(0)) → CU(less_int(neg(0), neg(mult_nat(s(s(0)), 0))), pos(s(0)))

The TRS R consists of the following rules:

mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(mult_nat(s(s(0)), s(x1)))), minus_nat(0, x1))

The TRS R consists of the following rules:

mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(mult_nat(s(s(0)), s(x1)))), minus_nat(0, x1))

The TRS R consists of the following rules:

mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(mult_nat(s(s(0)), s(x1)))), minus_nat(0, x1)) at position [0,1,0] we obtained the following new rules [LPAR04]:

CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(plus_nat(mult_nat(s(0), s(x1)), s(x1)))), minus_nat(0, x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(plus_nat(mult_nat(s(0), s(x1)), s(x1)))), minus_nat(0, x1))

The TRS R consists of the following rules:

mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(plus_nat(mult_nat(s(0), s(x1)), s(x1)))), minus_nat(0, x1)) at position [0,1,0,0] we obtained the following new rules [LPAR04]:

CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(plus_nat(plus_nat(mult_nat(0, s(x1)), s(x1)), s(x1)))), minus_nat(0, x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(plus_nat(plus_nat(mult_nat(0, s(x1)), s(x1)), s(x1)))), minus_nat(0, x1))

The TRS R consists of the following rules:

mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(plus_nat(plus_nat(mult_nat(0, s(x1)), s(x1)), s(x1)))), minus_nat(0, x1))

The TRS R consists of the following rules:

mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(plus_nat(plus_nat(mult_nat(0, s(x1)), s(x1)), s(x1)))), minus_nat(0, x1)) at position [0,1,0,0,0] we obtained the following new rules [LPAR04]:

CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(plus_nat(plus_nat(0, s(x1)), s(x1)))), minus_nat(0, x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(plus_nat(plus_nat(0, s(x1)), s(x1)))), minus_nat(0, x1))

The TRS R consists of the following rules:

mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(plus_nat(plus_nat(0, s(x1)), s(x1)))), minus_nat(0, x1))

The TRS R consists of the following rules:

plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false

The set Q consists of the following terms:

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(plus_nat(plus_nat(0, s(x1)), s(x1)))), minus_nat(0, x1))

The TRS R consists of the following rules:

plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false

The set Q consists of the following terms:

plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(plus_nat(plus_nat(0, s(x1)), s(x1)))), minus_nat(0, x1)) at position [0,1,0,0] we obtained the following new rules [LPAR04]:

CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(plus_nat(s(x1), s(x1)))), minus_nat(0, x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(plus_nat(s(x1), s(x1)))), minus_nat(0, x1))

The TRS R consists of the following rules:

plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false

The set Q consists of the following terms:

plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(plus_nat(s(x1), s(x1)))), minus_nat(0, x1)) at position [0,1,0] we obtained the following new rules [LPAR04]:

CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(s(plus_nat(x1, s(x1))))), minus_nat(0, x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Rewriting

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(s(plus_nat(x1, s(x1))))), minus_nat(0, x1))

The TRS R consists of the following rules:

plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false

The set Q consists of the following terms:

plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, neg(s(x1))) → CU(less_int(neg(s(x1)), neg(s(plus_nat(x1, s(x1))))), minus_nat(0, x1)) at position [0] we obtained the following new rules [LPAR04]:

CU(true, neg(s(x1))) → CU(less_int(neg(x1), neg(plus_nat(x1, s(x1)))), minus_nat(0, x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Rewriting

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Rewriting

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(s(x1))) → CU(less_int(neg(x1), neg(plus_nat(x1, s(x1)))), minus_nat(0, x1))

The TRS R consists of the following rules:

plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false

The set Q consists of the following terms:

plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [LPAR04] the rule CU(true, neg(s(x1))) → CU(less_int(neg(x1), neg(plus_nat(x1, s(x1)))), minus_nat(0, x1)) at position [1] we obtained the following new rules [LPAR04]:

CU(true, neg(s(s(x0)))) → CU(less_int(neg(s(x0)), neg(plus_nat(s(x0), s(s(x0))))), neg(s(x0)))
CU(true, neg(s(0))) → CU(less_int(neg(0), neg(plus_nat(0, s(0)))), pos(0))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Rewriting

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Rewriting

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Narrowing

                                                                                                                              ↳ QDP

                                                                                                                                ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(s(s(x0)))) → CU(less_int(neg(s(x0)), neg(plus_nat(s(x0), s(s(x0))))), neg(s(x0)))
CU(true, neg(s(0))) → CU(less_int(neg(0), neg(plus_nat(0, s(0)))), pos(0))

The TRS R consists of the following rules:

plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false

The set Q consists of the following terms:

plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Rewriting

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Rewriting

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Narrowing

                                                                                                                              ↳ QDP

                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(s(s(x0)))) → CU(less_int(neg(s(x0)), neg(plus_nat(s(x0), s(s(x0))))), neg(s(x0)))

The TRS R consists of the following rules:

plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false

The set Q consists of the following terms:

plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Rewriting

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Rewriting

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Narrowing

                                                                                                                              ↳ QDP

                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ UsableRulesProof

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(s(s(x0)))) → CU(less_int(neg(s(x0)), neg(plus_nat(s(x0), s(s(x0))))), neg(s(x0)))

The TRS R consists of the following rules:

plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false
plus_nat(0, x) → x

The set Q consists of the following terms:

plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Rewriting

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Rewriting

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Narrowing

                                                                                                                              ↳ QDP

                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ UsableRulesProof

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ QReductionProof

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(s(s(x0)))) → CU(less_int(neg(s(x0)), neg(plus_nat(s(x0), s(s(x0))))), neg(s(x0)))

The TRS R consists of the following rules:

plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false
plus_nat(0, x) → x

The set Q consists of the following terms:

plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, neg(s(s(x0)))) → CU(less_int(neg(s(x0)), neg(plus_nat(s(x0), s(s(x0))))), neg(s(x0))) at position [0,1,0] we obtained the following new rules [LPAR04]:

CU(true, neg(s(s(x0)))) → CU(less_int(neg(s(x0)), neg(s(plus_nat(x0, s(s(x0)))))), neg(s(x0)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Rewriting

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Rewriting

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Narrowing

                                                                                                                              ↳ QDP

                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ UsableRulesProof

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ QReductionProof

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(s(s(x0)))) → CU(less_int(neg(s(x0)), neg(s(plus_nat(x0, s(s(x0)))))), neg(s(x0)))

The TRS R consists of the following rules:

plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false
plus_nat(0, x) → x

The set Q consists of the following terms:

plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule CU(true, neg(s(s(x0)))) → CU(less_int(neg(s(x0)), neg(s(plus_nat(x0, s(s(x0)))))), neg(s(x0))) at position [0] we obtained the following new rules [LPAR04]:

CU(true, neg(s(s(x0)))) → CU(less_int(neg(x0), neg(plus_nat(x0, s(s(x0))))), neg(s(x0)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Rewriting

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Rewriting

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Narrowing

                                                                                                                              ↳ QDP

                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ UsableRulesProof

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ QReductionProof

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ Rewriting

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

CU(true, neg(s(s(x0)))) → CU(less_int(neg(x0), neg(plus_nat(x0, s(s(x0))))), neg(s(x0)))

The TRS R consists of the following rules:

plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false
plus_nat(0, x) → x

The set Q consists of the following terms:

plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

CU(true, neg(s(s(x0)))) → CU(less_int(neg(x0), neg(plus_nat(x0, s(s(x0))))), neg(s(x0)))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0
POL(CU(x₁, x₂)) = x₂
POL(false) = 0
POL(less_int(x₁, x₂)) = 0
POL(neg(x₁)) = x₁
POL(plus_nat(x₁, x₂)) = x₁ + x₂
POL(s(x₁)) = 1 + x₁
POL(true) = 0

The following usable rules [FROCOS05] were oriented: none

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ UsableRulesProof

                                            ↳ QDP

                                              ↳ QReductionProof

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ UsableRulesProof

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ DependencyGraphProof

                                                                ↳ AND

                                                                  ↳ QDP

                                                                  ↳ QDP

                                                                    ↳ UsableRulesProof

                                                                      ↳ QDP

                                                                        ↳ QReductionProof

                                                                          ↳ QDP

                                                                            ↳ Narrowing

                                                                              ↳ QDP

                                                                                ↳ DependencyGraphProof

                                                                                  ↳ QDP

                                                                                    ↳ UsableRulesProof

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ UsableRulesProof

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ UsableRulesProof

                                                                                                          ↳ QDP

                                                                                                            ↳ QReductionProof

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Rewriting

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Rewriting

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Narrowing

                                                                                                                              ↳ QDP

                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ UsableRulesProof

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ QReductionProof

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ Rewriting

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ QDPOrderProof

                                                                                                                                                      ↳ QDP

                                                                                                                                                        ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(neg(s(x)), neg(0)) → true
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
less_int(neg(0), neg(0)) → false
less_int(neg(0), neg(s(y))) → false
plus_nat(0, x) → x

The set Q consists of the following terms:

plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.